Nuprl Lemma : nil_fseg
11,40
postcript
pdf
T
:Type,
l
:(
T
List). fseg(
T
;[];
l
)
latex
ProofTree
Definitions
type
List
,
[]
,
t
T
,
s
=
t
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
as
@
bs
,
,
Type
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
fseg(
T
;
L1
;
L2
)
,
Void
,
x
:
A
.
B
(
x
)
,
Top
,
S
T
,
s
~
t
Lemmas
append
nil
sq
,
member
wf
,
top
wf
,
append
wf
origin
T:Type, l:(T List). fseg(T;[];l)
T:Type, l:(T List). fseg(T;[];l)
T
B(x)x:A. B(x)
B(x)
x:A. B(x)
x:A.B(x)
T